FDL - Nuprl Definition : es-simul

Nuprl Definition : es-simul

11,40

e:s.P(s)@j
== (

x:Id. vartype(j;x)

r ds(x)?Top)
== c

(

e'@j. (e' < e)

(P(state after e')

(

e'':E. ((e' <loc e'') & (e' < e))))
== c

e'@j. (e < e')

(P((state when e'))

(

e'':E. ((e'' <loc e') & (e < e')))))

clarification:

es-simul(es;e;j;ds;s.P(s))
== (

x:Id. es-vartype(es; j; x)

r fpf-cap(ds;IdDeq;x;Top))
== c

(alle-at(es;j;e'.es-causl(es; e'; e)
== c

(P(es-state-after(es;e'))

(

e'':es-E(es). (es-locl(es; e'; e'') & es-causl(es; e'; e)))))
== c

& alle-at(es;j;e'.es-causl(es; e; e')
== c

(P(es-state-when(es;e'))
== c

(

e'':es-E(es). (es-locl(es; e''; e') & es-causl(es; e; e'))))))

Definitions A c B, x:A. B(x), Id, vartype(i;x), f(x)?z, IdDeq, Top, state after e, e@i. P(e), P Q, P Q, (state when e), x:A. B(x), E, P & Q, (e <loc e'), (e < e')

FDL editor aliases es-simul

Definitions	A c B, x:A. B(x), Id, vartype(i;x), f(x)?z, IdDeq, Top, state after e, e@i. P(e), P Q, P Q, (state when e), x:A. B(x), E, P & Q, (e <loc e'), (e < e')
FDL editor aliases	es-simul